Unfold `decidable` 0 THEN D ({-}2)